Nuprl Lemma : Namer_wf
11,40
postcript
pdf
n
:
,
Id_list
:(Id List). Namer(
n
;
Id_list
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Namer(
n
;
Id_list
)
,
P
&
Q
,
,
Lemmas
int
seg
wf
,
Id
wf
,
inject
wf
,
not
wf
,
l
member
wf
,
nat
wf
origin
n:
, Id_list:(Id List). Namer(n;Id_list) 
Type n:, Id_list:(Id List). Namer(n;Id_list) Type x:A. B(x) T